Inference at * 1 
Iof proof for Lemma p-lift wf:

.....subterm..... T:t1:n

1. A : Type
2. B : Type
3. P : A
4. d : x:ADec(P(x))
5. {x:A| P(x)} B
6. x : A
  d(x)  (P(x) + (P(x))) 

latex

 by (Fold `or` 0) 
CollapseTHEN ((Fold `decidable` 0) 
CollapseTHEN (Auto)) 

latex

C.

Definitions

f(a), t  T